aframe-p(es; i; k; L)
== alle-at(es;
== alle-at(i;
== alle-at(e.((es-kind(es; e) = k)
== alle-at( (x:Id. 
== alle-at( (((es_state_after(es; e)(x) = es_state_when(es; e)(x)))  (x  L))
== alle-at(  (((x  L))  (es_state_after(es; e)(x) = es_state_when(es; e)(x)))))) 

latex

---

clarification:

aframe-p(es; i; k; L)
== alle-at(es;
== alle-at(i;
== alle-at(e.((es-kind(es; e) = k  Knd)
== alle-at( (x:Id. 
== alle-at( (((es_state_after(es; e)(x)
== alle-at( (((=
== alle-at( (((es_state_when(es; e)(x)
== alle-at( ((( rationalses-vartype(es; i; x)))
== alle-at(  (x  L  Id))
== alle-at(  (((x  L  Id))
== alle-at(   (es_state_after(es; e)(x)
== alle-at(   (=
== alle-at(   (es_state_when(es; e)(x)
== alle-at(   ( rationalses-vartype(es; i; x)))))) 

latex

Definitions	alle-at(es; i; e.P(e)), Knd, es-kind(es; e), x:A. B(x), P  Q, P  Q, A, (x  l), Id, s = t, x:AB(x), rationals, es-vartype(es; i; x), es_state_after(es; e), f(a), es_state_when(es; e)
FDL editor aliases	aframe-p